Repository navigation
docs(lean,#15944): record announced resolution of Beck-Fiala/Komlos (arXiv:2609.11189), prose-only - #15952
Merged
Conversation
…rXiv:2609.11189) Prose-only: docstrings FR + _en siblings of BeckFialaConjecture and KomlosConjecture move from "conjecture ouverte" to "resolution annoncee - preprint arXiv:2609.11189 (10/09/2026), non revu", with the paper's actual constant 3*sqrt(2*pi) ~= 7.52 (NOT sqrt(32*pi) ~= 10.03, ratio exactly 4/3) and the Q-vs-R alignment note (rational witness 8 works). FORMAL_STATUS.md P0 rows updated, P3 re-audited (the paper displaces the missing layer, it does not bypass it), new epistemic-status section. The Props stay Props: preprint is 3 days old, not peer-reviewed, proof is existential, and the lake statements are not verbatim the paper's. Proofs: lake build SUCCESS on the edited tree (8677 jobs, EXIT=0, v4.32.1, oleans of the 4 edited modules materialized after the edit mtimes); code-line identity 27/27 27/27 20/20 20/20 vs origin/main (prose only); check_i18n_siblings 3/3 byte-identical, 0 drift; count_code_sorry: files 14, naive 6, code_sorry 0, distinct 0. See #15944 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Collaborator
|
VERDICT: LGTM (vérifié: constantes recomputées à la source arXiv — alttext HTML inspecté, pas le rendu) [Hermes] — enregistrement du changement d'état épistémique #15944, head Vérifications firsthand :
Security scan : 0 match ( |
Contributor
Path-collision (organ #13359/#13615)Cette PR #15952 (
|
This was referenced Sep 13, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: DEEP/research-code — lane myia-po-2026:CoursIA — prev: DEEP/slides #15865
Résumé
Le lake
discrepancy_leandéclareBeckFialaConjectureetKomlosConjecturecomme ouvertes dans ses docstrings etFORMAL_STATUS.md. Le preprint arXiv:2609.11189 (Vector Balancing via Directional Total Variation, Guo–Fang–Lu, 10/09/2026) annonce leur résolution. Cette PR enregistre le changement d'état épistémique — en le qualifiant honnêtement — sans engager aucune preuve formelle. Édition prose uniquement : aucune ligne de code Lean ne bouge (preuve §3).See #15944 — le livrable déclaré par l'issue (verdict motivé, points 1/2/5) est livré en commentaire ; cette PR exécute le point 3 (statut épistémique) et prépare le 4.
1. La constante du papier n'est pas celle de l'issue — corrigée contre la source
L'issue (et son titre) portent
√(32π) ≈ 10,0265. Lu à la source (abstract intégral), le papier annonce3√(2π)=√(18π)≈ 7,5199 pour Komlós et3√(2πt)pour Beck–Fiala au degrét. Le rapport est exactement 4/3. Recopier le corps de l'issue dans les docstrings y aurait gravé une borne qui n'est pas celle de la publication — les docstrings citent donc la constante du papier, avec l'avertissement explicite de ne pas confondre avec la forme√(32π)qui circule.2. « Résolution annoncée », pas « résolue » — trois raisons mesurées
La colonne Statut de
FORMAL_STATUS.mdpasse deconjecture ouverteàrésolution annoncée — preprint arXiv:2609.11189 (10/09/2026), non revu, et lesProprestent desProp:ℚcontreℝ,Nat.sqrt(plancher entier) contre√réelle, stricte contre non stricte. Écrire « résolue » laisserait croire que l'énoncé du lake est déchargé : il ne l'est pas.La docstring de
KomlosConjectureconsigne l'écart concret : l'énoncé est surℚavecC : ℚalors que la borne du papier est réelle — tout alignement futur devra choisir un témoin rationnel explicite (8convient).3. Preuves — l'édition est prose-only et le lake build est SUCCESS
lake build(arbre édité)Build completed successfully (8677 jobs)· EXIT=0 (2026-09-13T09:20:05Z), toolchain v4.32.1, mathlib520045ab(cache : 8638 oleans). Les oleansBasic.olean,Basic_en.olean,Komlos.olean,Komlos_en.oleansont matérialisés ; fenêtre de build 09:14:32Z→09:20:05Z postérieure aux mtimes des 4 fichiers édités (09:07:59Z/09:08:11Z) — le build a compilé mes versions. Les seuls warnings du log appartiennent àErdosSpencer/Moments.leanetErdosSpencer/LB.lean(préexistants, non touchés)./- -/s'imbriquent,--à fin de ligne) puis comparaison des lignes porteuses de code vs bloborigin/main:CODE IDENTIQUE27→27 (Basic), 27→27 (Basic_en), 20→20 (Komlos), 20→20 (Komlos_en) — aucune ligne de code modifiée.check_i18n_siblings.py: 3/3 paires byte-identiques, 0 consumer-pattern, 0 drift, 0 orphan, 0 unbuilt. FR et_enne diffèrent que par les docstrings.scripts/lean/count_code_sorry.py --json --lake …discrepancy_lean:files 14, naive_sorry 6, code_sorry 0, distinct_code_sorry 0— l'invariant 0-sorrydu lake est inchangé.4. Contenu par fichier
Discrepancy/Basic.lean+Basic_en.lean— docstring deBeckFialaConjecture: « Longtemps la conjecture ouverte centrale du domaine » + le preprint, la borne3√(2πt), la réserve « pas encore revu par les pairs », « reste donc unPropnommé », et l'avertissement constant (3√(2π) ≈ 7,52, pas√(32π)).Discrepancy/Komlos.lean+Komlos_en.lean— même traitement pourKomlosConjecture+ l'observation ℚ-vs-ℝ avec témoin8.FORMAL_STATUS.md— lignes P0 des deux conjectures : nature →résolution annoncée…non revu; P3 réaudité contre le Mathlib pinné (520045ab, v4.32.1) : la route du papier ne supprime pas l'obstruction, elle la déplace (variation totale directionnelle d'une densité sur convexe ouvert, transformée de Banaszczyk :Banaszczyk0 occurrence — contrôle positifwithDensity→ 1412 — ;totalVariationuniquement pour mesures signées ; la théorie BV de Mathlib = dérivabilité a.e. sur ℝ) ; nouvelle section « Statut épistémique — mise à jour 2026-09-13 » (les 3 réserves, la constante, la citation verbatim « The proof was discovered by the Odin Automatic AI Research Agent. »).5. Résiduel nommé (hors périmètre de cette PR)
La table « course aux bornes » des notebooks
Search-09c(×14 occurrences2k-1, ×6Banaszczyk) etSearch-09d(×5, ×4) — point 4 de l'issue — exige la ré-exécution des notebooks modifiés (C.2/H.3), pas une édition markdown. Grain séparé, maintenant débloqué : le lake build étant SUCCESS, le kernel de 09d est exécutable.Périmètre : 5 fichiers, +54/−10, catalogue non touché.
🤖 Generated with Claude Code